YES(?,O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).

Strict Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

The following argument positions are usable:
  Uargs(append) = {1, 2}, Uargs(::) = {2}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

    [append](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
                       [0 1]      [0 1]      [0]
                                                
  [append#1](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                       [0 1]      [0 1]      [0]
                                                
        [::](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
                       [0 1]      [0 1]      [2]
                                                
               [nil] = [2]
                       [1]
                          
     [appendAll](x1) = [1 1] x1 + [1]
                       [0 2]      [0]
                                     
   [appendAll#1](x1) = [1 1] x1 + [0]
                       [0 2]      [0]
                                     
    [appendAll2](x1) = [2 1] x1 + [1]
                       [0 2]      [0]
                                     
  [appendAll2#1](x1) = [2 1] x1 + [0]
                       [0 2]      [0]
                                     
    [appendAll3](x1) = [2 2] x1 + [2]
                       [2 2]      [0]
                                     
  [appendAll3#1](x1) = [2 2] x1 + [1]
                       [2 2]      [0]

This order satisfies following ordering constraints

            [append(@l1, @l2)] = [1 1] @l1 + [1 0] @l2 + [1]               
                                 [0 1]       [0 1]       [0]               
                               > [1 1] @l1 + [1 0] @l2 + [0]               
                                 [0 1]       [0 1]       [0]               
                               = [append#1(@l1, @l2)]                      
                                                                           
  [append#1(::(@x, @xs), @l2)] = [1 0] @l2 + [1 2] @x + [1 1] @xs + [3]    
                                 [0 1]       [0 1]      [0 1]       [2]    
                               > [1 0] @l2 + [1 1] @x + [1 1] @xs + [2]    
                                 [0 1]       [0 1]      [0 1]       [2]    
                               = [::(@x, append(@xs, @l2))]                
                                                                           
        [append#1(nil(), @l2)] = [1 0] @l2 + [3]                           
                                 [0 1]       [1]                           
                               > [1 0] @l2 + [0]                           
                                 [0 1]       [0]                           
                               = [@l2]                                     
                                                                           
               [appendAll(@l)] = [1 1] @l + [1]                            
                                 [0 2]      [0]                            
                               > [1 1] @l + [0]                            
                                 [0 2]      [0]                            
                               = [appendAll#1(@l)]                         
                                                                           
   [appendAll#1(::(@l1, @ls))] = [1 2] @l1 + [1 1] @ls + [3]               
                                 [0 2]       [0 2]       [4]               
                               > [1 1] @l1 + [1 1] @ls + [2]               
                                 [0 1]       [0 2]       [0]               
                               = [append(@l1, appendAll(@ls))]             
                                                                           
          [appendAll#1(nil())] = [3]                                       
                                 [2]                                       
                               > [2]                                       
                                 [1]                                       
                               = [nil()]                                   
                                                                           
              [appendAll2(@l)] = [2 1] @l + [1]                            
                                 [0 2]      [0]                            
                               > [2 1] @l + [0]                            
                                 [0 2]      [0]                            
                               = [appendAll2#1(@l)]                        
                                                                           
  [appendAll2#1(::(@l1, @ls))] = [2 3] @l1 + [2 1] @ls + [4]               
                                 [0 2]       [0 2]       [4]               
                               > [1 3] @l1 + [2 1] @ls + [3]               
                                 [0 2]       [0 2]       [0]               
                               = [append(appendAll(@l1), appendAll2(@ls))] 
                                                                           
         [appendAll2#1(nil())] = [5]                                       
                                 [2]                                       
                               > [2]                                       
                                 [1]                                       
                               = [nil()]                                   
                                                                           
              [appendAll3(@l)] = [2 2] @l + [2]                            
                                 [2 2]      [0]                            
                               > [2 2] @l + [1]                            
                                 [2 2]      [0]                            
                               = [appendAll3#1(@l)]                        
                                                                           
  [appendAll3#1(::(@l1, @ls))] = [2 4] @l1 + [2 2] @ls + [7]               
                                 [2 4]       [2 2]       [6]               
                               > [2 3] @l1 + [2 2] @ls + [4]               
                                 [0 2]       [2 2]       [0]               
                               = [append(appendAll2(@l1), appendAll3(@ls))]
                                                                           
         [appendAll3#1(nil())] = [7]                                       
                                 [6]                                       
                               > [2]                                       
                                 [1]                                       
                               = [nil()]                                   
                                                                           

Hurray, we answered YES(?,O(n^2))